Nuprl Lemma : cond_rel_star_equiv
4,23
postcript
pdf
T
:Type,
P
:(
T
Prop),
R1
,
E
:(
T
T
Prop).
(EquivRel
_1
,
_2
:
T
.
_1
E
_2
)
when
P
,
R1
=>
E
R1
preserves
P
when
P
,
R1
^* =>
E
latex
Definitions
P
Q
,
R
^*
,
R
preserves
P
,
when
P
,
R1
=>
R2
,
EquivRel
x
,
y
:
T
.
E
(
x
;
y
)
,
x
:
A
.
B
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
f
y
,
Prop
,
t
T
Lemmas
rel
star
of
equiv
,
rel
star
wf
,
cond
rel
star
monotone
,
equiv
rel
wf
,
cond
rel
implies
wf
,
preserved
by
wf
origin
T:Type, P:(T
Prop), R1, E:(TTProp).
when P, R1 => E R1 preserves P when P, R1^* => E T:Type, P:(TProp), R1, E:(TTProp).
when P, R1 => E R1 preserves P when P, R1^* => E 
x,y. t(x;y)
T